Step of Proof: add_functionality_wrt_lt
12,41
postcript
pdf
Inference at
*
1
I
of proof for Lemma
add
functionality
wrt
lt
:
1.
i1
:
2.
i2
:
3.
j1
:
4.
j2
:
5.
i1
<
j1
6.
i2
j2
(
i1
+
i2
) < (
j1
+
j2
)
latex
by ((BackThruLemma `lt_to_le`)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C
),(first_nat 3:n)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
(
i1
+
i2
+1)
(
j1
+
j2
)
C
.
Definitions
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
lt
to
le
origin